es:event_system{i:l}, e:es-E(es), x:Id, T:Type.
es-dtype(es; loc(e); x; T)
 (es-first(es; e))
 (es-when(es; x; e) = es-initially(es; loc(e); x)  T) 

latex

Definitions	event_system{i:l}, t  T, x:A. B(x), es-E(es), Id, Type, loc(e), es-dtype(es; i; x; T), es-first(es; e), b, es-initially(es; i; x), <a, b>, s = t, P  Q, es-init(es;e), es-when(es; x; e), sqequal(s; t)
Lemmas	es-when-init, es-init-elim, assert wf, es-first wf, es-dtype wf, es-loc wf, Id wf, es-E wf, event system wf